The type preservation proof is closed!

It required a few extra assumptions, in particular

• A well typed function declaration requires the formal parameters to be distinct
• The fresh variables in a function call must be disjoint from the formal parameters

Rudi says the former is very reasonable, but the implementation of function calls is so different from these formal semantics that the latter does not correspond directly.

Additionally there are two admits in subst_lemma. Both of these confuse me. There are assumptions in the context that should solve them, but they fail to unify for reasons I do not understand.

To give a more complete answer, we could stick to FMap, but then we need to show that the properties are "the same" for two maps that are equal under Map.Equals, i.e., we can replace maps with other maps that have the same key-value mappings and still get the same results. But maybe this is a good opportunity to throw out the very old and semi-maintained FMap anyway.

We should definitely switch to some more ergonomic maps and I have been happy with stdpp.fin_maps elsewhere.

I will merge this one first and consider the type preservation part of #2 done for now, then open a new issue for the maps.